ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da).
ecl-trans(x)  ecl-trans-tuple{i:l}(ds; da) 

latex

Definitions	x. t(x), x,y,z. t(x;y;z), ff, tt, False, P  Q, A, A  B, x,y,z,w. t(x;y;z;w), x,y. t(x;y), , outl(x), if b then t else f fi , isl(x), band(p; q), ecl-trans(x), t  T, x:A. B(x), x(s), prop{i:l}, x(s1,s2,s3), x(s1,s2,s3,s4), x(s1,s2)
Lemmas	Id wf, Knd wf, fpf wf, ecl wf, ecl-add-catch wf, ecl-add-throw wf, add-ecl-act wf, reset-ecl-tuple wf, bfalse wf, eq int wf, ifthenelse wf, combine-ecl-tuples2 wf, nat wf, le wf, lt int wf, band wf, bor wf, combine-ecl-tuples wf, bool wf, ma-valtype wf, decl-state wf, ecl-base-tuple wf, ecl-trans-tuple wf, ecl ind wf